Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

truncation level of lists #1917

Merged
merged 3 commits into from
Apr 15, 2024
Merged

truncation level of lists #1917

merged 3 commits into from
Apr 15, 2024

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Apr 14, 2024 •
edited
Loading

We add some more list functions and a proof that n.+2 truncated types give n.+2 truncated lists.

@Alizter Alizter requested a review from jdchristensen April 14, 2024 17:57
jdchristensen
jdchristensen approved these changes Apr 15, 2024
View reviewed changes
Copy link
Collaborator

@jdchristensen jdchristensen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, while it's unrelated to this PR, the list_pentagon result would fit better in Classes/implementations/list.v, right after app_assoc, as then this file wouldn't need to Require list.v.

theories/Spaces/List.v Outdated Show resolved Hide resolved
theories/Spaces/List.v Outdated Show resolved Hide resolved
theories/Spaces/List.v Outdated Show resolved Hide resolved
theories/Spaces/List.v Outdated Show resolved Hide resolved
@Alizter
Copy link
Collaborator Author

Alizter commented Apr 15, 2024

@jdchristensen I might do another cleanup after this where I move all the stuff in implmentations to Spaces so that we have all the list functions and lemmas in one place. What do you think?

@jdchristensen
Copy link
Collaborator

@jdchristensen I might do another cleanup after this where I move all the stuff in implmentations to Spaces so that we have all the list functions and lemmas in one place. What do you think?

Sounds fine. I guess that would mean that this file will still depend on some of the Classes library, then. Hmm, I just noticed that the existing list.v only needs canonical_names.v, not abstract_algebra.v, so that's a change that can also be made.

@Alizter
Copy link
Collaborator Author

Alizter commented Apr 15, 2024

I'm gonna remove the extra functions I added and leave that for the cleanup. I'll just keep the proof of the truncation level available here.

@Alizter Alizter changed the title more list functions + truncation level of lists truncation level of lists Apr 15, 2024
Alizter added 2 commits April 15, 2024 20:19
@Alizter
truncation level of lists
4a35479 
<!-- ps-id: be8baae8-7652-48c2-b90d-d5e4f6748147 -->

Signed-off-by: Ali Caglayan <[email protected]>
@Alizter
review comments
ece8fa6 
Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter force-pushed the ps/rr/more_list_functions___truncation_level_of_lists branch from e16ad63 to ece8fa6 Compare April 15, 2024 19:25
Alizter
Alizter commented Apr 15, 2024
View reviewed changes
theories/Spaces/List.v Outdated Show resolved Hide resolved
@jdchristensen
Copy link
Collaborator

LGTM.

@Alizter Alizter merged commit 8b2c106 into HoTT:master Apr 15, 2024
23 checks passed
@Alizter Alizter deleted the ps/rr/more_list_functions___truncation_level_of_lists branch April 15, 2024 21:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jdchristensen jdchristensen jdchristensen approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Alizter @jdchristensen